IdrisDoc: [builtins]

[builtins]

(~=~) : (x : a) -> (y : b) -> Type

Explicit heterogeneous ("John Major") equality. Use this when Idris
incorrectly chooses homogeneous equality for (=).

Fixity
Non-associative, precedence 5
b

the type of the right side

a

the type of the left side

x

the left side

y

the right side

world : World -> prim__WorldType
void : Void -> a

The eliminator for the Void type.

unsafePerformPrimIO : PrimIO a -> a
unsafePerformIO : IO' ffi a -> a
trans : (a = b) -> (b = c) -> a = c

Transitivity of propositional equality

sym : (left = right) -> right = left

Symmetry of propositional equality

run__provider : IO a -> PrimIO a
run__IO : IO' ffi () -> PrimIO ()
rewrite__impl : (P : a -> Type) -> (x = y) -> P y -> P x

Perform substitution in a term according to some equality.

Like replace, but with an explicit predicate, and applying the rewrite
in the other direction, which puts it in a form usable by the rewrite
tactic and term.

replace : (x = y) -> P x -> P y

Perform substitution in a term according to some equality.

really_believe_me : a -> b

Subvert the type checker. This function will reduce in the type checker.
Use it with extreme care - it can result in segfaults or worse!

prim_write : String -> IO' l Int
prim_read : IO' l String
prim_pokeSingle : Ptr -> Int -> Double -> IO Int

Single precision floats are marshalled to Doubles

prim_pokePtr : Ptr -> Int -> Ptr -> IO Int
prim_pokeDouble : Ptr -> Int -> Double -> IO Int
prim_poke8 : Ptr -> Int -> Bits8 -> IO Int
prim_poke64 : Ptr -> Int -> Bits64 -> IO Int
prim_poke32 : Ptr -> Int -> Bits32 -> IO Int
prim_poke16 : Ptr -> Int -> Bits16 -> IO Int
prim_peekSingle : Ptr -> Int -> IO Double

Single precision floats are marshalled to Doubles

prim_peekPtr : Ptr -> Int -> IO Ptr
prim_peekDouble : Ptr -> Int -> IO Double
prim_peek8 : Ptr -> Int -> IO Bits8
prim_peek64 : Ptr -> Int -> IO Bits64
prim_peek32 : Ptr -> Int -> IO Bits32
prim_peek16 : Ptr -> Int -> IO Bits16
prim_lenString : String -> Int
prim_io_pure : a -> PrimIO a
prim_io_bind : PrimIO a -> (a -> PrimIO b) -> PrimIO b
prim_fwrite : Ptr -> String -> IO' l Int
prim_freadChars : Int -> Ptr -> IO' l String
prim_fread : Ptr -> IO' l String
prim_fork : PrimIO () -> PrimIO Ptr
prim__zextInt_BigInt : Int -> Integer
prim__zextInt_B64 : Int -> Bits64
prim__zextInt_B32 : Int -> Bits32
prim__zextInt_B16 : Int -> Bits16
prim__zextChar_BigInt : Char -> Integer
prim__zextB8_Int : Bits8 -> Int
prim__zextB8_BigInt : Bits8 -> Integer
prim__zextB8_B64 : Bits8 -> Bits64
prim__zextB8_B32 : Bits8 -> Bits32
prim__zextB8_B16 : Bits8 -> Bits16
prim__zextB64_BigInt : Bits64 -> Integer
prim__zextB32_Int : Bits32 -> Int
prim__zextB32_BigInt : Bits32 -> Integer
prim__zextB32_B64 : Bits32 -> Bits64
prim__zextB16_Int : Bits16 -> Int
prim__zextB16_BigInt : Bits16 -> Integer
prim__zextB16_B64 : Bits16 -> Bits64
prim__zextB16_B32 : Bits16 -> Bits32
prim__xorInt : Int -> Int -> Int
prim__xorChar : Char -> Char -> Char
prim__xorBigInt : Integer -> Integer -> Integer
prim__xorB8 : Bits8 -> Bits8 -> Bits8
prim__xorB64 : Bits64 -> Bits64 -> Bits64
prim__xorB32 : Bits32 -> Bits32 -> Bits32
prim__xorB16 : Bits16 -> Bits16 -> Bits16
prim__writeString : prim__WorldType -> String -> Int
prim__writeFile : prim__WorldType -> Ptr -> String -> Int
prim__vm : prim__WorldType -> Ptr
prim__uremInt : Int -> Int -> Int
prim__uremChar : Char -> Char -> Char
prim__uremBigInt : Integer -> Integer -> Integer
prim__uremB8 : Bits8 -> Bits8 -> Bits8
prim__uremB64 : Bits64 -> Bits64 -> Bits64
prim__uremB32 : Bits32 -> Bits32 -> Bits32
prim__uremB16 : Bits16 -> Bits16 -> Bits16
prim__udivInt : Int -> Int -> Int
prim__udivChar : Char -> Char -> Char
prim__udivBigInt : Integer -> Integer -> Integer
prim__udivB8 : Bits8 -> Bits8 -> Bits8
prim__udivB64 : Bits64 -> Bits64 -> Bits64
prim__udivB32 : Bits32 -> Bits32 -> Bits32
prim__udivB16 : Bits16 -> Bits16 -> Bits16
prim__truncInt_B8 : Int -> Bits8
prim__truncInt_B64 : Int -> Bits64
prim__truncInt_B32 : Int -> Bits32
prim__truncInt_B16 : Int -> Bits16
prim__truncBigInt_Int : Integer -> Int
prim__truncBigInt_Char : Integer -> Char
prim__truncBigInt_B8 : Integer -> Bits8
prim__truncBigInt_B64 : Integer -> Bits64
prim__truncBigInt_B32 : Integer -> Bits32
prim__truncBigInt_B16 : Integer -> Bits16
prim__truncB64_Int : Bits64 -> Int
prim__truncB64_B8 : Bits64 -> Bits8
prim__truncB64_B32 : Bits64 -> Bits32
prim__truncB64_B16 : Bits64 -> Bits16
prim__truncB32_Int : Bits32 -> Int
prim__truncB32_B8 : Bits32 -> Bits8
prim__truncB32_B16 : Bits32 -> Bits16
prim__truncB16_Int : Bits16 -> Int
prim__truncB16_B8 : Bits16 -> Bits8
prim__toStrInt : Int -> String
prim__toStrChar : Char -> String
prim__toStrBigInt : Integer -> String
prim__toStrB8 : Bits8 -> String
prim__toStrB64 : Bits64 -> String
prim__toStrB32 : Bits32 -> String
prim__toStrB16 : Bits16 -> String
prim__toFloatInt : Int -> Double
prim__toFloatChar : Char -> Double
prim__toFloatBigInt : Integer -> Double
prim__toFloatB8 : Bits8 -> Double
prim__toFloatB64 : Bits64 -> Double
prim__toFloatB32 : Bits32 -> Double
prim__toFloatB16 : Bits16 -> Double
prim__systemInfo : Int -> String
prim__syntactic_eq : (a : Type) -> (b : Type) -> (x : a) -> (y : b) -> Maybe (x = y)
prim__subInt : Int -> Int -> Int
prim__subFloat : Double -> Double -> Double
prim__subChar : Char -> Char -> Char
prim__subBigInt : Integer -> Integer -> Integer
prim__subB8 : Bits8 -> Bits8 -> Bits8
prim__subB64 : Bits64 -> Bits64 -> Bits64
prim__subB32 : Bits32 -> Bits32 -> Bits32
prim__subB16 : Bits16 -> Bits16 -> Bits16
prim__strToFloat : String -> Double
prim__strTail : String -> String
prim__strSubstr : Int -> Int -> String -> String
prim__strRev : String -> String
prim__strIndex : String -> Int -> Char
prim__strHead : String -> Char
prim__strCons : Char -> String -> String
prim__stdout : Ptr
prim__stdin : Ptr
prim__stderr : Ptr
prim__sremInt : Int -> Int -> Int
prim__sremChar : Char -> Char -> Char
prim__sremBigInt : Integer -> Integer -> Integer
prim__sremB8 : Bits8 -> Bits8 -> Bits8
prim__sremB64 : Bits64 -> Bits64 -> Bits64
prim__sremB32 : Bits32 -> Bits32 -> Bits32
prim__sremB16 : Bits16 -> Bits16 -> Bits16
prim__slteInt : Int -> Int -> Int
prim__slteFloat : Double -> Double -> Int
prim__slteChar : Char -> Char -> Int
prim__slteBigInt : Integer -> Integer -> Int
prim__slteB8 : Bits8 -> Bits8 -> Int
prim__slteB64 : Bits64 -> Bits64 -> Int
prim__slteB32 : Bits32 -> Bits32 -> Int
prim__slteB16 : Bits16 -> Bits16 -> Int
prim__sltInt : Int -> Int -> Int
prim__sltFloat : Double -> Double -> Int
prim__sltChar : Char -> Char -> Int
prim__sltBigInt : Integer -> Integer -> Int
prim__sltB8 : Bits8 -> Bits8 -> Int
prim__sltB64 : Bits64 -> Bits64 -> Int
prim__sltB32 : Bits32 -> Bits32 -> Int
prim__sltB16 : Bits16 -> Bits16 -> Int
prim__sizeofPtr : Int
prim__shlInt : Int -> Int -> Int
prim__shlChar : Char -> Char -> Char
prim__shlBigInt : Integer -> Integer -> Integer
prim__shlB8 : Bits8 -> Bits8 -> Bits8
prim__shlB64 : Bits64 -> Bits64 -> Bits64
prim__shlB32 : Bits32 -> Bits32 -> Bits32
prim__shlB16 : Bits16 -> Bits16 -> Bits16
prim__sgteInt : Int -> Int -> Int
prim__sgteFloat : Double -> Double -> Int
prim__sgteChar : Char -> Char -> Int
prim__sgteBigInt : Integer -> Integer -> Int
prim__sgteB8 : Bits8 -> Bits8 -> Int
prim__sgteB64 : Bits64 -> Bits64 -> Int
prim__sgteB32 : Bits32 -> Bits32 -> Int
prim__sgteB16 : Bits16 -> Bits16 -> Int
prim__sgtInt : Int -> Int -> Int
prim__sgtFloat : Double -> Double -> Int
prim__sgtChar : Char -> Char -> Int
prim__sgtBigInt : Integer -> Integer -> Int
prim__sgtB8 : Bits8 -> Bits8 -> Int
prim__sgtB64 : Bits64 -> Bits64 -> Int
prim__sgtB32 : Bits32 -> Bits32 -> Int
prim__sgtB16 : Bits16 -> Bits16 -> Int
prim__sextInt_BigInt : Int -> Integer
prim__sextInt_B64 : Int -> Bits64
prim__sextInt_B32 : Int -> Bits32
prim__sextInt_B16 : Int -> Bits16
prim__sextChar_BigInt : Char -> Integer
prim__sextB8_Int : Bits8 -> Int
prim__sextB8_BigInt : Bits8 -> Integer
prim__sextB8_B64 : Bits8 -> Bits64
prim__sextB8_B32 : Bits8 -> Bits32
prim__sextB8_B16 : Bits8 -> Bits16
prim__sextB64_BigInt : Bits64 -> Integer
prim__sextB32_Int : Bits32 -> Int
prim__sextB32_BigInt : Bits32 -> Integer
prim__sextB32_B64 : Bits32 -> Bits64
prim__sextB16_Int : Bits16 -> Int
prim__sextB16_BigInt : Bits16 -> Integer
prim__sextB16_B64 : Bits16 -> Bits64
prim__sextB16_B32 : Bits16 -> Bits32
prim__sdivInt : Int -> Int -> Int
prim__sdivChar : Char -> Char -> Char
prim__sdivBigInt : Integer -> Integer -> Integer
prim__sdivB8 : Bits8 -> Bits8 -> Bits8
prim__sdivB64 : Bits64 -> Bits64 -> Bits64
prim__sdivB32 : Bits32 -> Bits32 -> Bits32
prim__sdivB16 : Bits16 -> Bits16 -> Bits16
prim__registerPtr : Ptr -> Int -> ManagedPtr
prim__readString : prim__WorldType -> String
prim__readFile : prim__WorldType -> Ptr -> String
prim__readChars : prim__WorldType -> Int -> Ptr -> String
prim__ptrOffset : Ptr -> Int -> Ptr
prim__pokeSingle : prim__WorldType -> Ptr -> Int -> Double -> Int
prim__pokePtr : prim__WorldType -> Ptr -> Int -> Ptr -> Int
prim__pokeDouble : prim__WorldType -> Ptr -> Int -> Double -> Int
prim__poke8 : prim__WorldType -> Ptr -> Int -> Bits8 -> Int
prim__poke64 : prim__WorldType -> Ptr -> Int -> Bits64 -> Int
prim__poke32 : prim__WorldType -> Ptr -> Int -> Bits32 -> Int
prim__poke16 : prim__WorldType -> Ptr -> Int -> Bits16 -> Int
prim__peekSingle : prim__WorldType -> Ptr -> Int -> Double
prim__peekPtr : prim__WorldType -> Ptr -> Int -> Ptr
prim__peekDouble : prim__WorldType -> Ptr -> Int -> Double
prim__peek8 : prim__WorldType -> Ptr -> Int -> Bits8
prim__peek64 : prim__WorldType -> Ptr -> Int -> Bits64
prim__peek32 : prim__WorldType -> Ptr -> Int -> Bits32
prim__peek16 : prim__WorldType -> Ptr -> Int -> Bits16
prim__orInt : Int -> Int -> Int
prim__orChar : Char -> Char -> Char
prim__orBigInt : Integer -> Integer -> Integer
prim__orB8 : Bits8 -> Bits8 -> Bits8
prim__orB64 : Bits64 -> Bits64 -> Bits64
prim__orB32 : Bits32 -> Bits32 -> Bits32
prim__orB16 : Bits16 -> Bits16 -> Bits16
prim__null : Ptr
prim__negFloat : Double -> Double
prim__mulInt : Int -> Int -> Int
prim__mulFloat : Double -> Double -> Double
prim__mulChar : Char -> Char -> Char
prim__mulBigInt : Integer -> Integer -> Integer
prim__mulB8 : Bits8 -> Bits8 -> Bits8
prim__mulB64 : Bits64 -> Bits64 -> Bits64
prim__mulB32 : Bits32 -> Bits32 -> Bits32
prim__mulB16 : Bits16 -> Bits16 -> Bits16
prim__lteChar : Char -> Char -> Int
prim__lteBigInt : Integer -> Integer -> Int
prim__lteB8 : Bits8 -> Bits8 -> Int
prim__lteB64 : Bits64 -> Bits64 -> Int
prim__lteB32 : Bits32 -> Bits32 -> Int
prim__lteB16 : Bits16 -> Bits16 -> Int
prim__ltString : String -> String -> Int
prim__ltChar : Char -> Char -> Int
prim__ltBigInt : Integer -> Integer -> Int
prim__ltB8 : Bits8 -> Bits8 -> Int
prim__ltB64 : Bits64 -> Bits64 -> Int
prim__ltB32 : Bits32 -> Bits32 -> Int
prim__ltB16 : Bits16 -> Bits16 -> Int
prim__lshrInt : Int -> Int -> Int
prim__lshrChar : Char -> Char -> Char
prim__lshrBigInt : Integer -> Integer -> Integer
prim__lshrB8 : Bits8 -> Bits8 -> Bits8
prim__lshrB64 : Bits64 -> Bits64 -> Bits64
prim__lshrB32 : Bits32 -> Bits32 -> Bits32
prim__lshrB16 : Bits16 -> Bits16 -> Bits16
prim__intToChar : Int -> Char
prim__gteChar : Char -> Char -> Int
prim__gteBigInt : Integer -> Integer -> Int
prim__gteB8 : Bits8 -> Bits8 -> Int
prim__gteB64 : Bits64 -> Bits64 -> Int
prim__gteB32 : Bits32 -> Bits32 -> Int
prim__gteB16 : Bits16 -> Bits16 -> Int
prim__gtChar : Char -> Char -> Int
prim__gtBigInt : Integer -> Integer -> Int
prim__gtB8 : Bits8 -> Bits8 -> Int
prim__gtB64 : Bits64 -> Bits64 -> Int
prim__gtB32 : Bits32 -> Bits32 -> Int
prim__gtB16 : Bits16 -> Bits16 -> Int
prim__fromStrInt : String -> Int
prim__fromStrChar : String -> Char
prim__fromStrBigInt : String -> Integer
prim__fromStrB8 : String -> Bits8
prim__fromStrB64 : String -> Bits64
prim__fromStrB32 : String -> Bits32
prim__fromStrB16 : String -> Bits16
prim__fromFloatInt : Double -> Int
prim__fromFloatChar : Double -> Char
prim__fromFloatBigInt : Double -> Integer
prim__fromFloatB8 : Double -> Bits8
prim__fromFloatB64 : Double -> Bits64
prim__fromFloatB32 : Double -> Bits32
prim__fromFloatB16 : Double -> Bits16
prim__floatToStr : Double -> String
prim__floatTan : Double -> Double
prim__floatSqrt : Double -> Double
prim__floatSin : Double -> Double
prim__floatLog : Double -> Double
prim__floatFloor : Double -> Double
prim__floatExp : Double -> Double
prim__floatCos : Double -> Double
prim__floatCeil : Double -> Double
prim__floatATan : Double -> Double
prim__floatASin : Double -> Double
prim__floatACos : Double -> Double
prim__eqString : String -> String -> Int
prim__eqPtr : Ptr -> Ptr -> Int
prim__eqManagedPtr : ManagedPtr -> ManagedPtr -> Int
prim__eqInt : Int -> Int -> Int
prim__eqFloat : Double -> Double -> Int
prim__eqChar : Char -> Char -> Int
prim__eqBigInt : Integer -> Integer -> Int
prim__eqB8 : Bits8 -> Bits8 -> Int
prim__eqB64 : Bits64 -> Bits64 -> Int
prim__eqB32 : Bits32 -> Bits32 -> Int
prim__eqB16 : Bits16 -> Bits16 -> Int
prim__divFloat : Double -> Double -> Double
prim__concat : String -> String -> String
prim__complInt : Int -> Int
prim__complChar : Char -> Char
prim__complBigInt : Integer -> Integer
prim__complB8 : Bits8 -> Bits8
prim__complB64 : Bits64 -> Bits64
prim__complB32 : Bits32 -> Bits32
prim__complB16 : Bits16 -> Bits16
prim__charToInt : Char -> Int
prim__believe_me : (a : Type) -> (b : Type) -> (x : a) -> b
prim__ashrInt : Int -> Int -> Int
prim__ashrChar : Char -> Char -> Char
prim__ashrBigInt : Integer -> Integer -> Integer
prim__ashrB8 : Bits8 -> Bits8 -> Bits8
prim__ashrB64 : Bits64 -> Bits64 -> Bits64
prim__ashrB32 : Bits32 -> Bits32 -> Bits32
prim__ashrB16 : Bits16 -> Bits16 -> Bits16
prim__asPtr : ManagedPtr -> Ptr
prim__andInt : Int -> Int -> Int
prim__andChar : Char -> Char -> Char
prim__andBigInt : Integer -> Integer -> Integer
prim__andB8 : Bits8 -> Bits8 -> Bits8
prim__andB64 : Bits64 -> Bits64 -> Bits64
prim__andB32 : Bits32 -> Bits32 -> Bits32
prim__andB16 : Bits16 -> Bits16 -> Bits16
prim__addInt : Int -> Int -> Int
prim__addFloat : Double -> Double -> Double
prim__addChar : Char -> Char -> Char
prim__addBigInt : Integer -> Integer -> Integer
prim__addB8 : Bits8 -> Bits8 -> Bits8
prim__addB64 : Bits64 -> Bits64 -> Bits64
prim__addB32 : Bits32 -> Bits32 -> Bits32
prim__addB16 : Bits16 -> Bits16 -> Bits16
par : Lazy a -> a
mkForeignPrim : ForeignPrimType xs env t
liftPrimIO : (World -> PrimIO a) -> IO' l a
io_pure : a -> IO' l a
io_bind : IO' l a -> (a -> IO' l b) -> IO' l b
idris_crash : (msg : String) -> a

Abort immediately with an error message

foreign : (f : FFI) -> (fname : ffi_fn f) -> (ty : Type) -> {auto fty : FTy f [] ty} -> ty

Call a foreign function.

The particular semantics of foreign function calls depend on the
Idris compiler backend in use. For the default C backend, see the
documentation for FFI_C.

For more details, please consult the Idris documentation.

f

an FFI descriptor, which is specific to the compiler backend.

fname

the name of the foreign function

ty

the Idris type for the foreign function

fty

an automatically-found proof that the Idris type works with
the FFI in question

call__IO : IO' ffi a -> PrimIO a
believe_me : a -> b

Subvert the type checker. This function is abstract, so it will not reduce in
the type checker. Use it with care - it can result in segfaults or worse!

assert_unreachable : a

Assert to the totality checker that the case using this expression
is unreachable

assert_total : a -> a

Assert to the totality checker that the given expression will always
terminate.

assert_smaller : (x : a) -> (y : b) -> b

Assert to the totality checker that y is always structurally smaller than
x (which is typically a pattern argument, and must be in normal form
for this to work)

x

the larger value (typically a pattern argument)

y

the smaller value (typically an argument to a recursive call)

WorldRes : Type -> Type
data World : Type

A token representing the world, for use in IO

TheWorld : prim__WorldType -> World
data Void : Type

The empty type, also known as the trivially false proposition.

Use void or absurd to prove anything if you have a variable of type Void in scope.

data Unit : Type

The canonical single-element type, also known as the trivially
true proposition.

MkUnit : ()

The trivial constructor for ().

data Symbol_ : String -> Type

For 'symbol syntax. 'foo becomes Symbol_ "foo"

Ptr : Type
data PrimIO : Type -> Type

Idris's primitive IO, for building abstractions on top of

Prim__IO : a -> PrimIO a
PE_with block in with block in Decidable.Equality.Decidable.Equality.List a implementation of Decidable.Equality.DecEq, method decEq_a22721a1 : (x : String) -> (xs : List String) -> (ys : List String) -> (warg : Dec (xs = ys)) -> Dec (x :: xs = x :: ys)
PE_with block in with block in Decidable.Equality.Decidable.Equality.List a implementation of Decidable.Equality.DecEq, method decEq_1793dbad : (x : String) -> (xs : List String) -> (y : String) -> (p : (x = y) -> Void) -> (ys : List String) -> (warg : Dec (xs = ys)) -> Dec (x :: xs = y :: ys)
PE_with block in with block in Decidable.Equality.Decidable.Equality.(a, b) implementation of Decidable.Equality.DecEq, method decEq_fcee5068 : (a1 : Int) -> (a' : Int) -> (p : (a1 = a') -> Void) -> (b1 : Int) -> (b' : Int) -> (warg : Dec (b1 = b')) -> Dec ((a1, b1) = (a', b'))
PE_with block in with block in Decidable.Equality.Decidable.Equality.(a, b) implementation of Decidable.Equality.DecEq, method decEq_3386ce6a : (a1 : Int) -> (b1 : Int) -> (b' : Int) -> (warg : Dec (b1 = b')) -> Dec ((a1, b1) = (a1, b'))
PE_with block in Decidable.Equality.Decidable.Equality.List a implementation of Decidable.Equality.DecEq, method decEq_877d271a : (x : String) -> (xs : List String) -> (y : String) -> (warg : Dec (x = y)) -> (ys : List String) -> Dec (x :: xs = y :: ys)
PE_with block in Decidable.Equality.Decidable.Equality.(a, b) implementation of Decidable.Equality.DecEq, method decEq_e85079e4 : (a1 : Int) -> (a' : Int) -> (warg : Dec (a1 = a')) -> (b1 : Int) -> (b' : Int) -> Dec ((a1, b1) = (a', b'))
PE_uninhabited_d88e9ae7 : Void -> Void
PE_traverse_bc89cf0d : (a -> Maybe b) -> Binder a -> Maybe (Binder b)
PE_toNat_d6648df : Int -> Nat
PE_toNat_abb9c3f3 : Char -> Nat
PE_succ_dc75de74 : Nat -> Nat
PE_succ_d6648df : Int -> Int
PE_succ_abb9c3f3 : Char -> Char
PE_succ_85d79e7b : Integer -> Integer
PE_show_e3fee02 : (x : Bits64) -> String
PE_show_e3e405d : (x : Bits32) -> String
PE_show_e3d389f : (x : Bits16) -> String
PE_show_dc75de74 : (x : Nat) -> String
PE_show_d9a4e6b4 : (x : Bits8) -> String
PE_show_d6648df : (x : Int) -> String
PE_show_d6279dd5 : (x : ()) -> String
PE_show_d2fe2214 : (x : Bool) -> String
PE_show_ce35da4c : (x : TT) -> String
PE_show_bfb5fb44 : (x : FileError) -> String
PE_show_abb9c3f3 : (x : Char) -> String
PE_show_96c756fb : (x : Erasure) -> String
PE_show_85d79e7b : (x : Integer) -> String
PE_show_81ff5c9 : (x : String) -> String
PE_show_503ce65b : (x : Plicity) -> String
PE_show_27aba9f0 : (x : TTName) -> String
PE_show_21dfb116 : (x : NativeTy) -> String
PE_showPrec_f77535b0 : (d : Prec) -> (x : TTUExp) -> String
PE_showPrec_f53656e0 : (d : Prec) -> (x : List TTName) -> String
PE_showPrec_e41bdaf : (d : Prec) -> (x : Bits8) -> String
PE_showPrec_e19f790c : (d : Prec) -> (x : Const) -> String
PE_showPrec_d63daea2 : (d : Prec) -> (x : Bits64) -> String
PE_showPrec_d6064c5d : (d : Prec) -> (x : Bits32) -> String
PE_showPrec_d5e44cdf : (d : Prec) -> (x : Bits16) -> String
PE_showPrec_c1eaf49 : (d : Prec) -> (x : String) -> String
PE_showPrec_c17a9d73 : (d : Prec) -> (x : SpecialName) -> String
PE_showPrec_ba2f651f : (d : Prec) -> (x : Int) -> String
PE_showPrec_afbc3cbc : (d : Prec) -> (x : ArithTy) -> String
PE_showPrec_984f68c : (d : Prec) -> (x : List (TTName, TT)) -> String
PE_showPrec_95fe9cd0 : (d : Prec) -> (x : Binder TT) -> String
PE_showPrec_94f1242a : (d : Prec) -> (x : TT) -> String
PE_showPrec_88815844 : (d : Prec) -> (x : SourceLocation) -> String
PE_showPrec_81d0650b : (d : Prec) -> (x : (Int, Int)) -> String
PE_showPrec_75e9e4d5 : (d : Prec) -> (x : CtorArg) -> String
PE_showPrec_74c231e7 : (d : Prec) -> (x : NameType) -> String
PE_showPrec_7200248c : (d : Prec) -> (x : Double) -> String
PE_showPrec_6fb236cd : (d : Prec) -> (x : Erasure) -> String
PE_showPrec_6b468553 : (d : Prec) -> (x : List String) -> String
PE_showPrec_5dd5d41e : (d : Prec) -> (x : NativeTy) -> String
PE_showPrec_5da91fd6 : (d : Prec) -> (x : List FunArg) -> String
PE_showPrec_594a415 : (d : Prec) -> (x : TyDecl) -> String
PE_showPrec_57d9b224 : (d : Prec) -> (x : Plicity) -> String
PE_showPrec_52204d93 : (d : Prec) -> (x : Binder Raw) -> String
PE_showPrec_43e0032f : (d : Prec) -> (x : FunArg) -> String
PE_showPrec_40cb6e4b : (d : Prec) -> (x : Integer) -> String
PE_showPrec_32c264fb : (d : Prec) -> (x : Bool) -> String
PE_showPrec_2f63c032 : (d : Prec) -> (x : Raw) -> String
PE_showPrec_2a00f3d9 : (d : Prec) -> (x : IntTy) -> String
PE_showPrec_22f242c8 : (d : Prec) -> (x : Char) -> String
PE_showPrec_1e1ce584 : (d : Prec) -> (x : Err) -> String
PE_showPrec_1d20e84e : (d : Prec) -> (x : TTName) -> String
PE_showArg_ffac5032 : (x : List TTName) -> String
PE_showArg_e3fee02 : (x : Bits64) -> String
PE_showArg_e3e405d : (x : Bits32) -> String
PE_showArg_e3d389f : (x : Bits16) -> String
PE_showArg_d9a4e6b4 : (x : Bits8) -> String
PE_showArg_d6648df : (x : Int) -> String
PE_showArg_d2fe2214 : (x : Bool) -> String
PE_showArg_ce35da4c : (x : TT) -> String
PE_showArg_cc8900f4 : (x : List FunArg) -> String
PE_showArg_bb0fb4b : (x : (Int, Int)) -> String
PE_showArg_b942e4a0 : (x : Const) -> String
PE_showArg_b5e0f956 : (x : Double) -> String
PE_showArg_abb9c3f3 : (x : Char) -> String
PE_showArg_96c756fb : (x : Erasure) -> String
PE_showArg_95e1f2d3 : (x : Binder Raw) -> String
PE_showArg_94d47a2d : (x : Raw) -> String
PE_showArg_85d79e7b : (x : Integer) -> String
PE_showArg_8526d113 : (x : IntTy) -> String
PE_showArg_81ff5c9 : (x : String) -> String
PE_showArg_7c68e0ac : (x : List (TTName, TT)) -> String
PE_showArg_779d49d9 : (x : List String) -> String
PE_showArg_71ee6e6f : (x : ArithTy) -> String
PE_showArg_62f4334e : (x : SpecialName) -> String
PE_showArg_503ce65b : (x : Plicity) -> String
PE_showArg_4a5d0c80 : (x : Binder TT) -> String
PE_showArg_360b4f31 : (x : TTUExp) -> String
PE_showArg_32ae960f : (x : SourceLocation) -> String
PE_showArg_2a5375de : (x : NameType) -> String
PE_showArg_27aba9f0 : (x : TTName) -> String
PE_showArg_21dfb116 : (x : NativeTy) -> String
PE_showArg_21164daa : (x : FunArg) -> String
PE_showArg_106d7b4f : (x : Err) -> String
PE_quotedTy_f97db2b0 : TT
PE_quotedTy_ee737a41 : TT
PE_quotedTy_e56e5b7e : TT
PE_quotedTy_d7db5bba : Raw
PE_quotedTy_bce1e464 : Raw
PE_quotedTy_b31ae937 : TT
PE_quotedTy_a4a53738 : TT
PE_quotedTy_9338ed3f : Raw
PE_quotedTy_7e0e4c3b : TT
PE_quotedTy_6f584024 : Raw
PE_quotedTy_5da3a65e : TT
PE_quotedTy_5aa8d556 : Raw
PE_quotedTy_57b6a547 : Raw
PE_quotedTy_541df23c : TT
PE_quotedTy_503bdd31 : TT
PE_quotedTy_3fd6f596 : Raw
PE_quotedTy_394b4043 : Raw
PE_quotedTy_390ce668 : TT
PE_quotedTy_2a297d09 : TT
PE_quotedTy_29332ac5 : Raw
PE_quotedTy_1677322b : Raw
PE_quotedTy_12179418 : Raw
PE_quote_fc019d51 : IntTy -> TT
PE_quote_fac8d188 : NativeTy -> TT
PE_quote_fa93cf7e : TTUExp -> TT
PE_quote_fa569582 : Raw -> Raw
PE_quote_f74ccb34 : NameType -> Raw
PE_quote_f609a407 : Nat -> TT
PE_quote_e55d77da : (TTName, List CtorArg, Raw) -> Raw
PE_quote_e46b23c7 : Universe -> Raw
PE_quote_e3ac48c : Bits8 -> Raw
PE_quote_d7dc3a17 : String -> TT
PE_quote_d346d368 : String -> Raw
PE_quote_d17d363 : SourceLocation -> TT
PE_quote_d131bdb8 : NameType -> TT
PE_quote_c751e1f : Bits32 -> Raw
PE_quote_c18a3d6a : Integer -> Raw
PE_quote_bce2c2c1 : FunArg -> TT
PE_quote_b7217b5f : Nat -> Raw
PE_quote_b684ea12 : Const -> Raw
PE_quote_b07962c : List String -> TT
PE_quote_aff59616 : SourceLocation -> Raw
PE_quote_afc38062 : TyConArg -> Raw
PE_quote_ac50ef72 : Bits64 -> Raw
PE_quote_a9d591dc : Universe -> TT
PE_quote_975e5ce5 : List ConstructorDefn -> Raw
PE_quote_93c65b63 : Bits32 -> TT
PE_quote_9339cb9c : Raw -> TT
PE_quote_8e03b301 : Erasure -> TT
PE_quote_8c122a20 : Bits8 -> TT
PE_quote_7f2a32a0 : Char -> TT
PE_quote_7c189dea : IntTy -> Raw
PE_quote_7a3b5c56 : Integer -> TT
PE_quote_79604ae6 : List ErrorReportPart -> Raw
PE_quote_76b910df : Tactic -> TT
PE_quote_6fbef909 : Double -> Raw
PE_quote_6f591e81 : ErrorReportPart -> TT
PE_quote_6bddb20e : List String -> Raw
PE_quote_683cf56a : Double -> TT
PE_quote_66c35b6e : TT -> TT
PE_quote_6453dcf2 : Char -> Raw
PE_quote_62b348e9 : CtorArg -> Raw
PE_quote_5bffe9f8 : ArithTy -> Raw
PE_quote_5aa9b3b3 : TyConArg -> TT
PE_quote_5a6044f5 : ErrorReportPart -> Raw
PE_quote_5959da96 : Int -> Raw
PE_quote_591e7145 : FunArg -> Raw
PE_quote_57b783a4 : TTName -> TT
PE_quote_550a1776 : (List CtorArg, Raw) -> Raw
PE_quote_53c658fd : NativeTy -> Raw
PE_quote_52cd04a4 : Bits64 -> TT
PE_quote_4f9883b0 : List CtorArg -> Raw
PE_quote_4e8b4e80 : TTName -> Raw
PE_quote_4e5d6985 : Erasure -> Raw
PE_quote_4dbe8328 : Tactic -> Raw
PE_quote_4cf115a8 : TTUExp -> Raw
PE_quote_4b5a3ac7 : Const -> TT
PE_quote_4a689398 : List ConstructorDefn -> TT
PE_quote_49065bc8 : List FunArg -> Raw
PE_quote_478eee7a : List TyConArg -> TT
PE_quote_3fd7d3f3 : ConstructorDefn -> TT
PE_quote_3f4952b0 : Plicity -> TT
PE_quote_3f121f8e : TT -> Raw
PE_quote_3d5619d2 : Bits16 -> Raw
PE_quote_3ab5a8a2 : ConstructorDefn -> Raw
PE_quote_39501405 : List TyConArg -> Raw
PE_quote_394c1ea0 : CtorArg -> TT
PE_quote_2a782671 : List ErrorReportPart -> TT
PE_quote_29944289 : ArithTy -> TT
PE_quote_29340922 : List CtorArg -> TT
PE_quote_28a66304 : Bits16 -> TT
PE_quote_2856ff09 : Plicity -> Raw
PE_quote_19fbd576 : Int -> TT
PE_quote_16781088 : (TTName, List CtorArg, Raw) -> TT
PE_quote_12187275 : (List CtorArg, Raw) -> TT
PE_quote_11bb3e3a : List FunArg -> TT
PE_pure_c4df80b5 : a -> IO' ffi a
PE_pure_bd364ca1 : a -> Elab a
PE_pure_b70f061b : a -> Maybe a
PE_pure_837faffc : a -> IO' (MkFFI C_Types String String) a
PE_pack_3b7d037f : List Char -> String
PE_neutral_fc2e868 : String
PE_neutral_3b7d03e2 : List b
PE_neutral_3b7d03c1 : List a
PE_negate_d6648df : Int -> Int
PE_negate_b5e0f956 : Double -> Double
PE_negate_85d79e7b : Integer -> Integer
PE_map_e84935b3 : (func : a -> b) -> List a -> List b
PE_map_e3fc06f9 : (func : a -> b) -> Elab a -> Elab b
PE_map_729111da : (func : a -> b) -> Stream a -> Stream b
PE_map_622baa6c : (func : a -> b) -> IO' (MkFFI C_Types String String) a -> IO' (MkFFI C_Types String String) b
PE_isSuffixOf_22f242c8 : List Char -> List Char -> Bool
PE_isPrefixOf_22f242c8 : List Char -> List Char -> Bool
PE_isInfixOf_22f242c8 : List Char -> List Char -> Bool
PE_fromNat_d6648df : Nat -> Int
PE_fromNat_abb9c3f3 : Nat -> Char
PE_fromInteger_e3fee02 : Integer -> Bits64
PE_fromInteger_e3e405d : Integer -> Bits32
PE_fromInteger_e3d389f : Integer -> Bits16
PE_fromInteger_dc75de74 : Integer -> Nat
PE_fromInteger_d9a4e6b4 : Integer -> Bits8
PE_fromInteger_d6648df : Integer -> Int
PE_fromInteger_b5e0f956 : Integer -> Double
PE_fromInteger_85d79e7b : Integer -> Integer
PE_foldr_f16fec77 : (func : elem -> acc -> acc) -> (init : acc) -> (input : List elem) -> acc
PE_foldr_e148009f : (func : elem -> acc -> acc) -> (init : acc) -> (input : Binder elem) -> acc
PE_foldr_940a166a : (func : elem -> acc -> acc) -> (init : acc) -> (input : Maybe elem) -> acc
PE_foldl_f16fec77 : (func : acc -> elem -> acc) -> (init : acc) -> (input : List elem) -> acc
PE_enumFrom_dc75de74 : Nat -> Stream Nat
PE_enumFrom_d6648df : Int -> Stream Int
PE_enumFrom_abb9c3f3 : Char -> Stream Char
PE_enumFrom_85d79e7b : Integer -> Stream Integer
PE_elem_22f242c8 : Char -> List Char -> Bool
PE_decEq_c1eaf49 : (x1 : String) -> (x2 : String) -> Dec (x1 = x2)
PE_decEq_ba2f651f : (x1 : Int) -> (x2 : Int) -> Dec (x1 = x2)
PE_decEq_88815844 : (x1 : SourceLocation) -> (x2 : SourceLocation) -> Dec (x1 = x2)
PE_decEq_81d0650b : (x1 : (Int, Int)) -> (x2 : (Int, Int)) -> Dec (x1 = x2)
PE_decEq_6b468553 : (x1 : List String) -> (x2 : List String) -> Dec (x1 = x2)
PE_decEq_6b31ad5c : (x1 : Nat) -> (x2 : Nat) -> Dec (x1 = x2)
PE_decEq_32c264fb : (x1 : Bool) -> (x2 : Bool) -> Dec (x1 = x2)
PE_countFrom_ba2f651f : Int -> Int -> Stream Int
PE_countFrom_6b31ad5c : Nat -> Nat -> Stream Nat
PE_countFrom_40cb6e4b : Integer -> Integer -> Stream Integer
PE_constructor of Prelude.Algebra.Monoid#Semigroup ty_fc2e868 : Semigroup String
PE_constructor of Prelude.Algebra.Monoid#Semigroup ty_3b7d03e2 : Semigroup (List b)
PE_constructor of Prelude.Algebra.Monoid#Semigroup ty_3b7d03c1 : Semigroup (List a)
PE_concat_2278c957 : List (List a) -> List a
PE_concatMap_8faac41f : (a -> List b) -> List a -> List b
PE_concatMap_296b1ec9 : (a -> String) -> List a -> String
PE_compare_c1eaf49 : String -> String -> Ordering
PE_compare_ba2f651f : Int -> Int -> Ordering
PE_compare_9b1b58ef : () -> () -> Ordering
PE_compare_7200248c : Double -> Double -> Ordering
PE_compare_6b31ad5c : Nat -> Nat -> Ordering
PE_compare_40cb6e4b : Integer -> Integer -> Ordering
PE_compare_32c264fb : Bool -> Bool -> Ordering
PE_compare_22f242c8 : Char -> Char -> Ordering
PE_compare_1676ea41 : Prec -> Prec -> Ordering
PE_cast_dd2c0e30 : (orig : String) -> Integer
PE_cast_c71d3746 : (orig : Nat) -> Int
PE_cast_b8ccd99c : (orig : Char) -> Int
PE_cast_abf8387c : (orig : Integer) -> Nat
PE_cast_a18abc1e : (orig : String) -> List Char
PE_cast_8c354935 : (orig : Int) -> Nat
PE_cast_569d416 : (orig : Int) -> Integer
PE_cast_4a482be : (orig : Nat) -> Integer
PE_cast_1f219304 : (orig : Int) -> Char
PE_any_45711470 : (a -> Bool) -> List a -> Bool
PE_absurd_654c8984 : (h : Void) -> a
PE_abs_d6648df : Int -> Int
PE_abs_85d79e7b : Integer -> Integer
PE_Prelude.Show.List a implementation of Prelude.Show.Show, method show_9d4f9763 : (x : List (TTName, TT)) -> String
PE_Prelude.Show.List a implementation of Prelude.Show.Show, method show_81ff5c9 : (x : List String) -> String
PE_Prelude.Show.List a implementation of Prelude.Show.Show, method show_27aba9f0 : (x : List TTName) -> String
PE_Prelude.Show.List a implementation of Prelude.Show.Show, method show_21164daa : (x : List FunArg) -> String
PE_Prelude.Show.List a implementation of Prelude.Show.Show, method showPrec_c1eaf49 : (d : Prec) -> (x : List String) -> String
PE_Prelude.Show.List a implementation of Prelude.Show.Show, method showPrec_47428422 : (d : Prec) -> (x : List (TTName, TT)) -> String
PE_Prelude.Show.List a implementation of Prelude.Show.Show, method showPrec_43e0032f : (d : Prec) -> (x : List FunArg) -> String
PE_Prelude.Show.List a implementation of Prelude.Show.Show, method showPrec_1d20e84e : (d : Prec) -> (x : List TTName) -> String
PE_Prelude.Show.(a, b) implementation of Prelude.Show.Show, method show_4ea7f87d : (x : (TTName, TT)) -> String
PE_Prelude.Show.(a, b) implementation of Prelude.Show.Show, method show_2d973430 : (x : (Int, Int)) -> String
PE_Prelude.Show.(a, b) implementation of Prelude.Show.Show, method showPrec_e07dba86 : (d : Prec) -> (x : (Int, Int)) -> String
PE_Prelude.Show.(a, b) implementation of Prelude.Show.Show, method showPrec_23a70877 : (d : Prec) -> (x : (TTName, TT)) -> String
PE_Prelude.List.List a implementation of Prelude.Interfaces.Eq, method /=_c1eaf49 : List String -> List String -> Bool
PE_Prelude.Interfaces.(a, b) implementation of Prelude.Interfaces.Eq, method ==_e07dba86 : (Int, Int) -> (Int, Int) -> Bool
PE_Prelude.Interfaces.(a, b) implementation of Prelude.Interfaces.Eq, method /=_e07dba86 : (Int, Int) -> (Int, Int) -> Bool
PE_List a, TT implementation of Language.Reflection.Quotable_fc2e868 : Quotable (List String) TT
PE_List a, TT implementation of Language.Reflection.Quotable_df2fadf0 : Quotable (List ErrorReportPart) TT
PE_List a, TT implementation of Language.Reflection.Quotable_d09dc8b8 : Quotable (List TyConArg) TT
PE_List a, TT implementation of Language.Reflection.Quotable_7915b8f7 : Quotable (List (TTName, List CtorArg, Raw)) TT
PE_List a, TT implementation of Language.Reflection.Quotable_33ab986c : Quotable (List ConstructorDefn) TT
PE_List a, TT implementation of Language.Reflection.Quotable_20086ef3 : Quotable (List FunArg) TT
PE_List a, TT implementation of Language.Reflection.Quotable_1507bcbc : Quotable (List CtorArg) TT
PE_List a, Raw implementation of Language.Reflection.Quotable_fc2e868 : Quotable (List String) Raw
PE_List a, Raw implementation of Language.Reflection.Quotable_df2fadf0 : Quotable (List ErrorReportPart) Raw
PE_List a, Raw implementation of Language.Reflection.Quotable_d09dc8b8 : Quotable (List TyConArg) Raw
PE_List a, Raw implementation of Language.Reflection.Quotable_7915b8f7 : Quotable (List (TTName, List CtorArg, Raw)) Raw
PE_List a, Raw implementation of Language.Reflection.Quotable_33ab986c : Quotable (List ConstructorDefn) Raw
PE_List a, Raw implementation of Language.Reflection.Quotable_20086ef3 : Quotable (List FunArg) Raw
PE_List a, Raw implementation of Language.Reflection.Quotable_1507bcbc : Quotable (List CtorArg) Raw
PE_List a implementation of Prelude.Show.Show_fc2e868 : Show (List String)
PE_List a implementation of Prelude.Show.Show_94989888 : Show (List TTName)
PE_List a implementation of Prelude.Show.Show_3b11ed4e : Show (List (TTName, TT))
PE_List a implementation of Prelude.Show.Show_20086ef3 : Show (List FunArg)
PE_List a implementation of Prelude.Interfaces.Eq_fc2e868 : Eq (List String)
PE_List a implementation of Decidable.Equality.DecEq_fc2e868 : DecEq (List String)
PE_Language.Reflection.Utils.Binder a implementation of Prelude.Show.Show, method show_ce35da4c : (x : Binder TT) -> String
PE_Language.Reflection.Utils.Binder a implementation of Prelude.Show.Show, method show_94d47a2d : (x : Binder Raw) -> String
PE_Language.Reflection.Utils.Binder a implementation of Prelude.Show.Show, method showPrec_94f1242a : (d : Prec) -> (x : Binder TT) -> String
PE_Language.Reflection.Utils.Binder a implementation of Prelude.Show.Show, method showPrec_2f63c032 : (d : Prec) -> (x : Binder Raw) -> String
PE_Language.Reflection.Utils.Binder a implementation of Prelude.Interfaces.Eq, method /=_94f1242a : Binder TT -> Binder TT -> Bool
PE_Language.Reflection.Utils.Binder a implementation of Prelude.Interfaces.Eq, method /=_2f63c032 : Binder Raw -> Binder Raw -> Bool
PE_Language.Reflection.List a, TT implementation of Language.Reflection.Quotable, method quotedTy_fc2e868 : TT
PE_Language.Reflection.List a, TT implementation of Language.Reflection.Quotable, method quotedTy_df2fadf0 : TT
PE_Language.Reflection.List a, TT implementation of Language.Reflection.Quotable, method quotedTy_d09dc8b8 : TT
PE_Language.Reflection.List a, TT implementation of Language.Reflection.Quotable, method quotedTy_7915b8f7 : TT
PE_Language.Reflection.List a, TT implementation of Language.Reflection.Quotable, method quotedTy_33ab986c : TT
PE_Language.Reflection.List a, TT implementation of Language.Reflection.Quotable, method quotedTy_20086ef3 : TT
PE_Language.Reflection.List a, TT implementation of Language.Reflection.Quotable, method quotedTy_1507bcbc : TT
PE_Language.Reflection.List a, TT implementation of Language.Reflection.Quotable, method quote_e456e031 : List TyConArg -> TT
PE_Language.Reflection.List a, TT implementation of Language.Reflection.Quotable, method quote_c5256c59 : List ErrorReportPart -> TT
PE_Language.Reflection.List a, TT implementation of Language.Reflection.Quotable, method quote_b5ff547f : List CtorArg -> TT
PE_Language.Reflection.List a, TT implementation of Language.Reflection.Quotable, method quote_a91ea646 : List ConstructorDefn -> TT
PE_Language.Reflection.List a, TT implementation of Language.Reflection.Quotable, method quote_9bccd82b : List (TTName, List CtorArg, Raw) -> TT
PE_Language.Reflection.List a, TT implementation of Language.Reflection.Quotable, method quote_81ff5c9 : List String -> TT
PE_Language.Reflection.List a, TT implementation of Language.Reflection.Quotable, method quote_21164daa : List FunArg -> TT
PE_Language.Reflection.List a, Raw implementation of Language.Reflection.Quotable, method quotedTy_fc2e868 : Raw
PE_Language.Reflection.List a, Raw implementation of Language.Reflection.Quotable, method quotedTy_df2fadf0 : Raw
PE_Language.Reflection.List a, Raw implementation of Language.Reflection.Quotable, method quotedTy_d09dc8b8 : Raw
PE_Language.Reflection.List a, Raw implementation of Language.Reflection.Quotable, method quotedTy_7915b8f7 : Raw
PE_Language.Reflection.List a, Raw implementation of Language.Reflection.Quotable, method quotedTy_33ab986c : Raw
PE_Language.Reflection.List a, Raw implementation of Language.Reflection.Quotable, method quotedTy_20086ef3 : Raw
PE_Language.Reflection.List a, Raw implementation of Language.Reflection.Quotable, method quotedTy_1507bcbc : Raw
PE_Language.Reflection.List a, Raw implementation of Language.Reflection.Quotable, method quote_e456e031 : List TyConArg -> Raw
PE_Language.Reflection.List a, Raw implementation of Language.Reflection.Quotable, method quote_c5256c59 : List ErrorReportPart -> Raw
PE_Language.Reflection.List a, Raw implementation of Language.Reflection.Quotable, method quote_b5ff547f : List CtorArg -> Raw
PE_Language.Reflection.List a, Raw implementation of Language.Reflection.Quotable, method quote_a91ea646 : List ConstructorDefn -> Raw
PE_Language.Reflection.List a, Raw implementation of Language.Reflection.Quotable, method quote_9bccd82b : List (TTName, List CtorArg, Raw) -> Raw
PE_Language.Reflection.List a, Raw implementation of Language.Reflection.Quotable, method quote_81ff5c9 : List String -> Raw
PE_Language.Reflection.List a, Raw implementation of Language.Reflection.Quotable, method quote_21164daa : List FunArg -> Raw
PE_Language.Reflection.Binder implementation of Prelude.Traversable.Traversable, method traverse_b6e9086d : (a -> Maybe b) -> Binder a -> Maybe (Binder b)
PE_Language.Reflection.(a, b), TT implementation of Language.Reflection.Quotable, method quotedTy_4f9883b0 : TT
PE_Language.Reflection.(a, b), TT implementation of Language.Reflection.Quotable, method quotedTy_1c1cafc1 : TT
PE_Language.Reflection.(a, b), TT implementation of Language.Reflection.Quotable, method quote_9fb2a838 : (TTName, List CtorArg, Raw) -> TT
PE_Language.Reflection.(a, b), TT implementation of Language.Reflection.Quotable, method quote_42a8fa14 : (List CtorArg, Raw) -> TT
PE_Language.Reflection.(a, b), Raw implementation of Language.Reflection.Quotable, method quotedTy_4f9883b0 : Raw
PE_Language.Reflection.(a, b), Raw implementation of Language.Reflection.Quotable, method quotedTy_1c1cafc1 : Raw
PE_Language.Reflection.(a, b), Raw implementation of Language.Reflection.Quotable, method quote_9fb2a838 : (TTName, List CtorArg, Raw) -> Raw
PE_Language.Reflection.(a, b), Raw implementation of Language.Reflection.Quotable, method quote_42a8fa14 : (List CtorArg, Raw) -> Raw
PE_Decidable.Equality.List a implementation of Decidable.Equality.DecEq, method decEq_c1eaf49 : (x1 : List String) -> (x2 : List String) -> Dec (x1 = x2)
PE_Decidable.Equality.(a, b) implementation of Decidable.Equality.DecEq, method decEq_e07dba86 : (x1 : (Int, Int)) -> (x2 : (Int, Int)) -> Dec (x1 = x2)
PE_Binder a implementation of Prelude.Show.Show_ce34fbef : Show (Binder Raw)
PE_Binder a implementation of Prelude.Show.Show_6356f717 : Show (Binder TT)
PE_Binder a implementation of Prelude.Interfaces.Eq_ce34fbef : Eq (Binder Raw)
PE_Binder a implementation of Prelude.Interfaces.Eq_6356f717 : Eq (Binder TT)
PE_>_e41bdaf : Bits8 -> Bits8 -> Bool
PE_>_d63daea2 : Bits64 -> Bits64 -> Bool
PE_>_d6064c5d : Bits32 -> Bits32 -> Bool
PE_>_d5e44cdf : Bits16 -> Bits16 -> Bool
PE_>_c1eaf49 : String -> String -> Bool
PE_>_ba2f651f : Int -> Int -> Bool
PE_>_9b1b58ef : () -> () -> Bool
PE_>_7200248c : Double -> Double -> Bool
PE_>_6b31ad5c : Nat -> Nat -> Bool
PE_>_40cb6e4b : Integer -> Integer -> Bool
PE_>_32c264fb : Bool -> Bool -> Bool
PE_>_22f242c8 : Char -> Char -> Bool
PE_>_1676ea41 : Prec -> Prec -> Bool
PE_>=_ba2f651f : Int -> Int -> Bool
PE_>=_22f242c8 : Char -> Char -> Bool
PE_>=_1676ea41 : Prec -> Prec -> Bool
PE_==_f77535b0 : TTUExp -> TTUExp -> Bool
PE_==_e41bdaf : Bits8 -> Bits8 -> Bool
PE_==_e19f790c : Const -> Const -> Bool
PE_==_d63daea2 : Bits64 -> Bits64 -> Bool
PE_==_d6064c5d : Bits32 -> Bits32 -> Bool
PE_==_d5e44cdf : Bits16 -> Bits16 -> Bool
PE_==_caeefbca : Ptr -> Ptr -> Bool
PE_==_c1eaf49 : String -> String -> Bool
PE_==_c17a9d73 : SpecialName -> SpecialName -> Bool
PE_==_ba2f651f : Int -> Int -> Bool
PE_==_afbc3cbc : ArithTy -> ArithTy -> Bool
PE_==_9b1b58ef : () -> () -> Bool
PE_==_95fe9cd0 : Binder TT -> Binder TT -> Bool
PE_==_94f1242a : TT -> TT -> Bool
PE_==_88815844 : SourceLocation -> SourceLocation -> Bool
PE_==_81d0650b : (Int, Int) -> (Int, Int) -> Bool
PE_==_74c231e7 : NameType -> NameType -> Bool
PE_==_7200248c : Double -> Double -> Bool
PE_==_6b468553 : List String -> List String -> Bool
PE_==_6b31ad5c : Nat -> Nat -> Bool
PE_==_5dd5d41e : NativeTy -> NativeTy -> Bool
PE_==_5a6178be : ManagedPtr -> ManagedPtr -> Bool
PE_==_52204d93 : Binder Raw -> Binder Raw -> Bool
PE_==_40cb6e4b : Integer -> Integer -> Bool
PE_==_39ea5141 : Universe -> Universe -> Bool
PE_==_346eb07c : Ordering -> Ordering -> Bool
PE_==_32c264fb : Bool -> Bool -> Bool
PE_==_2f63c032 : Raw -> Raw -> Bool
PE_==_2a00f3d9 : IntTy -> IntTy -> Bool
PE_==_22f242c8 : Char -> Char -> Bool
PE_==_1d20e84e : TTName -> TTName -> Bool
PE_==_1676ea41 : Prec -> Prec -> Bool
PE_<_e41bdaf : Bits8 -> Bits8 -> Bool
PE_<_d63daea2 : Bits64 -> Bits64 -> Bool
PE_<_d6064c5d : Bits32 -> Bits32 -> Bool
PE_<_d5e44cdf : Bits16 -> Bits16 -> Bool
PE_<_c1eaf49 : String -> String -> Bool
PE_<_ba2f651f : Int -> Int -> Bool
PE_<_9b1b58ef : () -> () -> Bool
PE_<_7200248c : Double -> Double -> Bool
PE_<_6b31ad5c : Nat -> Nat -> Bool
PE_<_40cb6e4b : Integer -> Integer -> Bool
PE_<_32c264fb : Bool -> Bool -> Bool
PE_<_22f242c8 : Char -> Char -> Bool
PE_<_1676ea41 : Prec -> Prec -> Bool
PE_<=_ba2f651f : Int -> Int -> Bool
PE_<=_6b31ad5c : Nat -> Nat -> Bool
PE_<=_40cb6e4b : Integer -> Integer -> Bool
PE_<=_22f242c8 : Char -> Char -> Bool
PE_<*>_b6e9086d : Maybe (a -> b) -> Maybe a -> Maybe b
PE_<$>_d4eefcf3 : (func : a -> b) -> Elab a -> Elab b
PE_/_7200248c : Double -> Double -> Double
PE_/=_ba2f651f : Int -> Int -> Bool
PE_/=_32c264fb : Bool -> Bool -> Bool
PE_-_ba2f651f : Int -> Int -> Int
PE_-_7200248c : Double -> Double -> Double
PE_-_40cb6e4b : Integer -> Integer -> Integer
PE_+_ba2f651f : Int -> Int -> Int
PE_+_7200248c : Double -> Double -> Double
PE_+_6b31ad5c : Nat -> Nat -> Nat
PE_+_40cb6e4b : Integer -> Integer -> Integer
PE_*_ba2f651f : Int -> Int -> Int
PE_*_7200248c : Double -> Double -> Double
PE_*_6b31ad5c : Nat -> Nat -> Nat
PE_*_40cb6e4b : Integer -> Integer -> Integer
PE_(a, b), TT implementation of Language.Reflection.Quotable_4e00078a : Quotable (TTName, List CtorArg, Raw) TT
PE_(a, b), TT implementation of Language.Reflection.Quotable_4799f661 : Quotable (List CtorArg, Raw) TT
PE_(a, b), Raw implementation of Language.Reflection.Quotable_4e00078a : Quotable (TTName, List CtorArg, Raw) Raw
PE_(a, b), Raw implementation of Language.Reflection.Quotable_4799f661 : Quotable (List CtorArg, Raw) Raw
PE_(a, b) implementation of Prelude.Show.Show_75bec382 : Show (Int, Int)
PE_(a, b) implementation of Prelude.Show.Show_5f781b07 : Show (TTName, TT)
PE_(a, b) implementation of Prelude.Interfaces.Eq_75bec382 : Eq (Int, Int)
PE_(a, b) implementation of Decidable.Equality.DecEq_75bec382 : DecEq (Int, Int)
MkFFI : (ffi_types : Type -> Type) -> (ffi_fn : Type) -> (ffi_data : Type) -> FFI
ffi_types

A family describing which types are available in the FFI

ffi_fn

The type used to specify the names of foreign functions in this FFI

ffi_data

How this FFI describes exported datatypes

ManagedPtr : Type
Lazy : Type -> Type

Lazily evaluated values.
At run time, the delayed value will only be computed when required by
a case split.

data JsFn : Type -> Type
MkJsFn : (x : t) -> JsFn t
data JS_Types : Type -> Type
JS_Str : JS_Types String
JS_Float : JS_Types Double
JS_Ptr : JS_Types Ptr
JS_Unit : JS_Types ()
JS_FnT : JS_FnTypes a -> JS_Types (JsFn a)
JS_IntT : JS_IntTypes i -> JS_Types i
data JS_IntTypes : Type -> Type
JS_IntChar : JS_IntTypes Char
JS_IntNative : JS_IntTypes Int
JS_IO : Type -> Type
data JS_FnTypes : Type -> Type
JS_Fn : JS_Types s -> JS_FnTypes t -> JS_FnTypes (s -> t)
JS_FnIO : JS_Types t -> JS_FnTypes (IO' l t)
JS_FnBase : JS_Types t -> JS_FnTypes t
Inf : Type -> Type

Possibly infinite data.
A value which may be infinite is accepted by the totality checker if
it appears under a data constructor. At run time, the delayed value will
only be computed when required by a case split.

data IO' : (lang : FFI) -> Type -> Type

The IO type, parameterised over the FFI that is available within
it.

MkIO : (World -> PrimIO (WorldRes a)) -> IO' lang a
IO : (res : Type) -> Type

Interactive programs, describing I/O actions and returning a value.

res

The result type of the program

ForeignPrimType : (xs : List Type) -> FEnv ffi xs -> Type -> Type
Force : Delayed t a -> a

Compute a value from a delayed computation.

Inserted by the elaborator where necessary.

Float : Type

Deprecated alias for Double, for the purpose of backwards
compatibility. Idris does not support 32 bit floats at present.

data FTy : FFI -> List Type -> Type -> Type
FRet : ffi_types f t -> FTy f xs (IO' f t)
FFun : ffi_types f s -> FTy f (s :: xs) t -> FTy f xs (s -> t)
FFI_JS : FFI

The JavaScript FFI. The strings naming functions in this API are
JavaScript code snippets, into which the arguments are substituted
for the placeholders %0, %1, etc.

record FFI 

An FFI specifier, which describes how a particular compiler
backend handles foreign function calls.

MkFFI : (ffi_types : Type -> Type) -> (ffi_fn : Type) -> (ffi_data : Type) -> FFI
ffi_types

A family describing which types are available in the FFI

ffi_fn

The type used to specify the names of foreign functions in this FFI

ffi_data

How this FFI describes exported datatypes

ffi_types : (rec : FFI) -> Type -> Type

A family describing which types are available in the FFI

ffi_fn : (rec : FFI) -> Type

The type used to specify the names of foreign functions in this FFI

ffi_data : (rec : FFI) -> Type

How this FFI describes exported datatypes

data Delayed : DelayReason -> Type -> Type

The underlying implementation of Lazy and Inf.

Delay : (val : a) -> Delayed t a

A delayed computation.

Delay is inserted automatically by the elaborator where necessary.

Note that compiled code gives Delay special semantics.

t

whether this is laziness from an infinite structure or lazy evaluation

a

the type of the eventual value

val

a computation that will produce a value

data DelayReason : Type

Two types of delayed computation: that arising from lazy functions, and that
arising from infinite data. They differ in their totality condition.

Infinite : DelayReason
LazyValue : DelayReason
CData : Type
data (=) : (x : A) -> (y : B) -> Type

The propositional equality type. A proof that x = y.

To use such a proof, pattern-match on it, and the two equal things will then need to be the same pattern.

Note: Idris's equality type is potentially heterogeneous, which means that it is possible to state equalities between values of potentially different types. However, Idris will attempt the homogeneous case unless it fails to typecheck.

You may need to use (~=~) to explicitly request heterogeneous equality.

A

the type of the left side of the equality

B

the type of the right side of the equality

Refl : x = x

A proof that x in fact equals x. To construct this, you must have already shown that both sides are in fact equal.

A

the type at which the equality is proven

x

the element shown to be equal to itself.